COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BASL30\.
C00004 ENDMK
C⊗;
\\M0BASL30;\.
\F0

\J	I consider Maurer's proposal on the whole excellent.  He has
an excellent grasp of what the problems are in mathematical theory
of computation, and he evidently has a good group of students working
on them.  I would be inclined to put less emphasis on verifying the
verifier itself, since it can be debugged and bugs that remain are
more likely to cause it to reject proper proofs of correctness rather
than to admit the kind of incorrect proofs people are likely to
generate.  In fact I have some doubt that the complete verification
of a verifier is feasible at this time so that progress may be a bit
discouraging.  Therefore, I wouldn't be surprised or offended if part
way through the project they found it desirable to change some of their
goals and pursue simpler problems exemplifying particular aspects of the
general verification problem.\.